theory k_mem_pool_Design
  imports k_mem_pool9 "~~/src/HOL/Word/Bits_Bit"
begin 

text{*Data Structures In the Design Level*}              
type_synonym pool_num = nat
type_synonym level_num = nat
type_synonym block_num = nat  
type_synonym time = nat 
type_synonym size = nat 
type_synonym poolDName = string
typedecl thread
(*return pointer*)
type_synonym ptr = nat
(*bitMap*)
type_synonym bits = "bit list"
datatype bitMap = l32 bits | g32 ptr
(*struct of block id*) 
type_synonym struct_block_id = "pool_num \<times> level_num  \<times> block_num"
type_synonym struct_block = "struct_block_id \<times> ptr"
(*services using mutex*)
datatype sevice = K_Mem_Pool_Alloc

(*struct of dlink*)
datatype dnode1 = head ptr | nex ptr
datatype dnode2 = tail ptr | pre ptr

type_synonym struct_dnode = "dnode1 \<times> dnode2"
(*Add size and pool_num*)
type_synonym BlockD = "( struct_block_id \<times> size \<times> block_state_type) tree"
  
record PoolD = zerolevelblocklist :: "BlockD list"
               name :: string
               buf :: ptr
               max_sz :: nat
               nmax :: nat
               nlevels :: nat  
               max_inline_level :: nat
               bMap :: bitMap
               freelist :: struct_dnode

record StateD = t_state :: "Thread \<Rightarrow> thread_state_type"
                pools :: "PoolD list"
                t_time :: nat
                waitq :: "Thread \<rightharpoonup>(time \<times> poolDName)"
                thOccupyMutex :: "Thread \<rightharpoonup> sevice"
                cur :: Thread              
                idset :: "ID set" 
                buf2Blockl0 :: "ptr \<rightharpoonup> struct_block_id"(*in which level_num\<times>block_num is 0\<times>0*)
                ptr2bitMap :: "ptr \<rightharpoonup> bits"
                ptr2block :: "ptr \<rightharpoonup> struct_block" 
     

  
  
  
  
  
  
  
  
  
  
  
end